COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	unique[f83,jmc]		The unique names assumption
C00004 00003		Perhaps A(Joe,Henry) should include ∃x y.x ≠ y or even
C00006 00004		Perhaps the most straightforward approach to the unique
C00011 00005	How about the axiom
C00013 ENDMK
C⊗;
unique[f83,jmc]		The unique names assumption

	Ray Reiter pointed out that the treatment proposed in
my letter to him didn't work.  Here's another try.

Suppose we want to conclude that Joe is different from Henry if
this is permitted by some knowledge A(Joe,Henry) that we are
taking into account.  We circumscribe the expression

	Joe = Henry

regarding Joe and Henry as variable - not taking
equality to be variable as previous
attempts tried to.  We get

(1)	A(Joe,Henry) ∧ 
	(∀Joe' Henry'.A(Joe',Henry') ∧ (Joe' = Henry' ⊃ Joe = Henry)
		⊃ (Joe = Henry ≡ Joe' = Henry')).

If the language contains constants  Joe0  and  Henry0  which are provably
distinct and such that  A(Joe0,Henry0)  is provable, then we can
substitute these individuals for  Joe'  and  Henry'.
The left side of (1) is then true, and we can conclude  Joe ≠ Henry.

This is a great simplification of our previous attempts, because
we don't have to bother with names as objects and denotation
as a function.  Nevertheless, finding the desired constants  Joe0
and  Henry0  may not always be feasible.  Indeed it may beg the
question.

	Perhaps A(Joe,Henry) should include ∃x y.x ≠ y or even
∃x y.person(x) ∧ person(y) ∧ x ≠ y.  This wouldn't suffice if
we had ten individuals and were expected to jump to the conclusion
that they are all distinct.  We would need a stronger axiom
asserting the existence of enough individuals of the desired
kind.

	This sort of works for inferring that two specific objects
are distinct if possible.  However, suppose we have a whole collection
of objects, and we want as many as possible to be distinct.  Extending
the above method to four objects gives a six way parallel circumscription
which is reducible to a single circumscription by Lifschitz's
trick - namely we circumscribe  E(x,z) defined by

	(z = 1 ∧ x1 = x2) ∨ (z = 2 ∧ x1 = x3) ∨ (z = 3 ∧ x2 = x3) ∨
(z = 4 ∧ x1 = x4) ∨ (z = 5 ∧ x2 = x4) ∨ (z = 6 ∧ x2 = x4)

as a predicate of z with x1, x2, . . . ,x6 variable.  We have

A(x1, ... ,x6) ∧ ∀x1' ... x6'.A(x1',...x6') ∧ (∀z.E(x',z) ⊃ E(x,z))
		⊃(∀z.E(x,z) ≡ E(x',z))
	Perhaps the most straightforward approach to the unique
names hypothesis  involves taking the names themselves as objects.
The following is taken from a draft written before Reiter pointed
out that the approach proposed doesn't quite work.
circum[f83,jmc]		AI Aplications of Circumscription

#. The unique names hypothesis

	Raymond Reiter (1979) introduced the phrase "unique names hypothesis"
for the assumption that distinct names denote distinct objects.  We want
to show how to handle this in a more general way by circumscription.

	Suppose we introduce names as objects, i.e. we introduce
⊗'John as a name for John.  For brevity we use the Lisp notation
⊗'John instead of the more usual "John".  We then assume an infinity
of first order axioms like

	%2'John ≠ 'Henry%1,

i.e. for every pair of distinct names there is such an axiom.

	From the
point of view of mathematical logic, there is no harm in having
an infinity of such axioms.  From the computational point of view of
a theorem proving or problem solving program, we
merely suppose that we rely on the computer to generate the assertion
that two names are distinct whenever this is required, since
a subroutine can easily tell whether two strings are the same.

	[One might suppose that some metamathematical considerations would
change from using an infinity of axioms, but usually this won't
be so, because we can generate an infinity of provably distinct
objects from a finite set of axioms.  All we need do is use
integers as names, axiomatize > as a relation including its
transitivity and have an axiom %2∀x_y.x_>_y_⊃_x_≠_y%1.  It is equally
feasible to finitely axiomatize strings in a way that ensures that
distinct strings are provably distinct.  The axiom systems required
can be much weaker than Peano arithmetic, since induction is not
required to prove particular instances of inequality.]

	One way of getting unique names is to use axioms like

!!a2:	%2name(John) = 'John%1

and

	%2name(Henry) = 'Henry%1.

The distinctness of names and the theory of inequality will then
give %2John_≠_Henry%1.

	However, this is too absolute for many applications.  It is
often preferable that objects denoted by distinct
names are to be presumed distinct unless there is reason to believe
them to be the same.  We can do this as follows.  Instead of
using axioms like ({eq a2}), we write

!!a3:	%2denotation('John) = John%1

and

	%2denotation('Henry) = Henry%1

Nothing now prevents  %2John = Henry%1, so we use the axiom

!!a4:	%2∀n1 n2. n1 ≠ n2 ∧ ¬ab aspecteq(n1,n2) ⊃ denotation n1 ≠ denotation n2%1.

	The idea of this axiom is that if ⊗n1 and ⊗n2 are distinct names,
and ⊗aspecteq(n1,n2) is not abnormal, i.e. does not satisfy the predicate
⊗ab, then ⊗n1 and ⊗n2 denote distinct objects.  When we have "taken into
account" all the facts we are going to take into account we will circumscribe
the expression  %2ab_z%1.  This will make %2ab_aspecteq(n1,n2)%1 false
unless some facts prevent it and hence will allow inferring that
 %2denotation_n1%1 and
%2denotation_n2%1 are distinct unless there is evidence that they are equal.

.skip 1
How about the axiom
¬ab aspect1 n ⊃ name den n = n.

Then if the names are different, the objects they denote will be
different unless something is abnormal.

What is considered to be variable?  Most likely it should be the
function  name.

Here's a try

'a ≠ 'b

den 'a = a

den 'b = b

We circumscribe  ab z  with  ab  and  name  as variable.  This gives

'a ≠ 'b ∧ den 'a = a ∧ den 'b = b ∧ ∀n.¬ab aspect1 n ⊃ name den n = n

∧ ∀name' ab'.((∀n.¬ab' aspect1 n ⊃ name' den n = n)
	      ∧ ∀z. ab' z ⊃ ab z
	      ⊃ ∀z.ab z ⊃ ab' z).

This doesn't work unless  a  and  b  are variable too.  Actually, den
must be variable.

Kreisel points out that the common assumption in geometry that
a collection of points is in generic position may be taken as
a non-monotonically generated hypothesis.  I suppose this would
also apply to the notion of generic model of an axiom system
as introduced in discussions of forcing.  I would conjecture that
if Etherington is right that equality cannot be handled by circumscription,
then genericity can't either.